; EXPECT: unsat
(set-logic ALL)
(set-option :incremental false)
(declare-fun x_1 () Bool)
(declare-fun x_2 () Bool)
(declare-fun x_3 () Bool)
(declare-fun x_4 () Bool)
(declare-fun x_5 () Bool)
(declare-fun x_6 () Bool)
(declare-fun x_7 () Bool)
(declare-fun x_8 () Bool)
(declare-fun x_9 () Bool)
(declare-fun x_10 () Bool)
(declare-fun x_11 () Bool)
(declare-fun x_12 () Bool)
(declare-fun x_13 () Bool)
(declare-fun x_14 () Bool)
(declare-fun x_15 () Bool)
(declare-fun x_16 () Bool)
(declare-fun x_17 () Bool)
(declare-fun x_18 () Bool)
(declare-fun x_19 () Bool)
(declare-fun x_20 () Bool)
(declare-fun x_21 () Bool)
(declare-fun x_22 () Bool)
(declare-fun x_23 () Bool)
(declare-fun x_24 () Bool)
(declare-fun x_25 () Bool)
(declare-fun x_26 () Bool)
(declare-fun x_27 () Bool)
(declare-fun x_28 () Bool)
(declare-fun x_29 () Bool)
(declare-fun x_30 () Bool)
(declare-fun x_31 () Bool)
(declare-fun x_32 () Bool)
(declare-fun x_33 () Bool)
(declare-fun x_34 () Bool)
(declare-fun x_35 () Bool)
(declare-fun x_36 () Bool)
(declare-fun x_37 () Bool)
(declare-fun x_38 () Bool)
(declare-fun x_39 () Bool)
(declare-fun x_40 () Bool)
(declare-fun x_41 () Bool)
(declare-fun x_42 () Bool)
(declare-fun x_43 () Bool)
(declare-fun x_44 () Bool)
(declare-fun x_45 () Bool)
(declare-fun x_46 () Bool)
(declare-fun x_47 () Bool)
(declare-fun x_48 () Bool)
(declare-fun x_49 () Bool)
(declare-fun x_50 () Bool)
(declare-fun x_51 () Bool)
(declare-fun x_52 () Bool)
(declare-fun x_53 () Bool)
(declare-fun x_54 () Bool)
(declare-fun x_55 () Bool)
(declare-fun x_56 () Bool)
(assert (or (not x_1) (not x_8)))
(assert (or (not x_1) (not x_15)))
(assert (or (not x_1) (not x_22)))
(assert (or (not x_1) (not x_29)))
(assert (or (not x_1) (not x_36)))
(assert (or (not x_1) (not x_43)))
(assert (or (not x_1) (not x_50)))
(assert (or (not x_8) (not x_15)))
(assert (or (not x_8) (not x_22)))
(assert (or (not x_8) (not x_29)))
(assert (or (not x_8) (not x_36)))
(assert (or (not x_8) (not x_43)))
(assert (or (not x_8) (not x_50)))
(assert (or (not x_15) (not x_22)))
(assert (or (not x_15) (not x_29)))
(assert (or (not x_15) (not x_36)))
(assert (or (not x_15) (not x_43)))
(assert (or (not x_15) (not x_50)))
(assert (or (not x_22) (not x_29)))
(assert (or (not x_22) (not x_36)))
(assert (or (not x_22) (not x_43)))
(assert (or (not x_22) (not x_50)))
(assert (or (not x_29) (not x_36)))
(assert (or (not x_29) (not x_43)))
(assert (or (not x_29) (not x_50)))
(assert (or (not x_36) (not x_43)))
(assert (or (not x_36) (not x_50)))
(assert (or (not x_43) (not x_50)))
(assert (or (not x_2) (not x_9)))
(assert (or (not x_2) (not x_16)))
(assert (or (not x_2) (not x_23)))
(assert (or (not x_2) (not x_30)))
(assert (or (not x_2) (not x_37)))
(assert (or (not x_2) (not x_44)))
(assert (or (not x_2) (not x_51)))
(assert (or (not x_9) (not x_16)))
(assert (or (not x_9) (not x_23)))
(assert (or (not x_9) (not x_30)))
(assert (or (not x_9) (not x_37)))
(assert (or (not x_9) (not x_44)))
(assert (or (not x_9) (not x_51)))
(assert (or (not x_16) (not x_23)))
(assert (or (not x_16) (not x_30)))
(assert (or (not x_16) (not x_37)))
(assert (or (not x_16) (not x_44)))
(assert (or (not x_16) (not x_51)))
(assert (or (not x_23) (not x_30)))
(assert (or (not x_23) (not x_37)))
(assert (or (not x_23) (not x_44)))
(assert (or (not x_23) (not x_51)))
(assert (or (not x_30) (not x_37)))
(assert (or (not x_30) (not x_44)))
(assert (or (not x_30) (not x_51)))
(assert (or (not x_37) (not x_44)))
(assert (or (not x_37) (not x_51)))
(assert (or (not x_44) (not x_51)))
(assert (or (not x_3) (not x_10)))
(assert (or (not x_3) (not x_17)))
(assert (or (not x_3) (not x_24)))
(assert (or (not x_3) (not x_31)))
(assert (or (not x_3) (not x_38)))
(assert (or (not x_3) (not x_45)))
(assert (or (not x_3) (not x_52)))
(assert (or (not x_10) (not x_17)))
(assert (or (not x_10) (not x_24)))
(assert (or (not x_10) (not x_31)))
(assert (or (not x_10) (not x_38)))
(assert (or (not x_10) (not x_45)))
(assert (or (not x_10) (not x_52)))
(assert (or (not x_17) (not x_24)))
(assert (or (not x_17) (not x_31)))
(assert (or (not x_17) (not x_38)))
(assert (or (not x_17) (not x_45)))
(assert (or (not x_17) (not x_52)))
(assert (or (not x_24) (not x_31)))
(assert (or (not x_24) (not x_38)))
(assert (or (not x_24) (not x_45)))
(assert (or (not x_24) (not x_52)))
(assert (or (not x_31) (not x_38)))
(assert (or (not x_31) (not x_45)))
(assert (or (not x_31) (not x_52)))
(assert (or (not x_38) (not x_45)))
(assert (or (not x_38) (not x_52)))
(assert (or (not x_45) (not x_52)))
(assert (or (not x_4) (not x_11)))
(assert (or (not x_4) (not x_18)))
(assert (or (not x_4) (not x_25)))
(assert (or (not x_4) (not x_32)))
(assert (or (not x_4) (not x_39)))
(assert (or (not x_4) (not x_46)))
(assert (or (not x_4) (not x_53)))
(assert (or (not x_11) (not x_18)))
(assert (or (not x_11) (not x_25)))
(assert (or (not x_11) (not x_32)))
(assert (or (not x_11) (not x_39)))
(assert (or (not x_11) (not x_46)))
(assert (or (not x_11) (not x_53)))
(assert (or (not x_18) (not x_25)))
(assert (or (not x_18) (not x_32)))
(assert (or (not x_18) (not x_39)))
(assert (or (not x_18) (not x_46)))
(assert (or (not x_18) (not x_53)))
(assert (or (not x_25) (not x_32)))
(assert (or (not x_25) (not x_39)))
(assert (or (not x_25) (not x_46)))
(assert (or (not x_25) (not x_53)))
(assert (or (not x_32) (not x_39)))
(assert (or (not x_32) (not x_46)))
(assert (or (not x_32) (not x_53)))
(assert (or (not x_39) (not x_46)))
(assert (or (not x_39) (not x_53)))
(assert (or (not x_46) (not x_53)))
(assert (or (not x_5) (not x_12)))
(assert (or (not x_5) (not x_19)))
(assert (or (not x_5) (not x_26)))
(assert (or (not x_5) (not x_33)))
(assert (or (not x_5) (not x_40)))
(assert (or (not x_5) (not x_47)))
(assert (or (not x_5) (not x_54)))
(assert (or (not x_12) (not x_19)))
(assert (or (not x_12) (not x_26)))
(assert (or (not x_12) (not x_33)))
(assert (or (not x_12) (not x_40)))
(assert (or (not x_12) (not x_47)))
(assert (or (not x_12) (not x_54)))
(assert (or (not x_19) (not x_26)))
(assert (or (not x_19) (not x_33)))
(assert (or (not x_19) (not x_40)))
(assert (or (not x_19) (not x_47)))
(assert (or (not x_19) (not x_54)))
(assert (or (not x_26) (not x_33)))
(assert (or (not x_26) (not x_40)))
(assert (or (not x_26) (not x_47)))
(assert (or (not x_26) (not x_54)))
(assert (or (not x_33) (not x_40)))
(assert (or (not x_33) (not x_47)))
(assert (or (not x_33) (not x_54)))
(assert (or (not x_40) (not x_47)))
(assert (or (not x_40) (not x_54)))
(assert (or (not x_47) (not x_54)))
(assert (or (not x_6) (not x_13)))
(assert (or (not x_6) (not x_20)))
(assert (or (not x_6) (not x_27)))
(assert (or (not x_6) (not x_34)))
(assert (or (not x_6) (not x_41)))
(assert (or (not x_6) (not x_48)))
(assert (or (not x_6) (not x_55)))
(assert (or (not x_13) (not x_20)))
(assert (or (not x_13) (not x_27)))
(assert (or (not x_13) (not x_34)))
(assert (or (not x_13) (not x_41)))
(assert (or (not x_13) (not x_48)))
(assert (or (not x_13) (not x_55)))
(assert (or (not x_20) (not x_27)))
(assert (or (not x_20) (not x_34)))
(assert (or (not x_20) (not x_41)))
(assert (or (not x_20) (not x_48)))
(assert (or (not x_20) (not x_55)))
(assert (or (not x_27) (not x_34)))
(assert (or (not x_27) (not x_41)))
(assert (or (not x_27) (not x_48)))
(assert (or (not x_27) (not x_55)))
(assert (or (not x_34) (not x_41)))
(assert (or (not x_34) (not x_48)))
(assert (or (not x_34) (not x_55)))
(assert (or (not x_41) (not x_48)))
(assert (or (not x_41) (not x_55)))
(assert (or (not x_48) (not x_55)))
(assert (or (not x_7) (not x_14)))
(assert (or (not x_7) (not x_21)))
(assert (or (not x_7) (not x_28)))
(assert (or (not x_7) (not x_35)))
(assert (or (not x_7) (not x_42)))
(assert (or (not x_7) (not x_49)))
(assert (or (not x_7) (not x_56)))
(assert (or (not x_14) (not x_21)))
(assert (or (not x_14) (not x_28)))
(assert (or (not x_14) (not x_35)))
(assert (or (not x_14) (not x_42)))
(assert (or (not x_14) (not x_49)))
(assert (or (not x_14) (not x_56)))
(assert (or (not x_21) (not x_28)))
(assert (or (not x_21) (not x_35)))
(assert (or (not x_21) (not x_42)))
(assert (or (not x_21) (not x_49)))
(assert (or (not x_21) (not x_56)))
(assert (or (not x_28) (not x_35)))
(assert (or (not x_28) (not x_42)))
(assert (or (not x_28) (not x_49)))
(assert (or (not x_28) (not x_56)))
(assert (or (not x_35) (not x_42)))
(assert (or (not x_35) (not x_49)))
(assert (or (not x_35) (not x_56)))
(assert (or (not x_42) (not x_49)))
(assert (or (not x_42) (not x_56)))
(assert (or (not x_49) (not x_56)))
(assert (or (or (or (or (or (or x_7 x_6) x_5) x_4) x_3) x_2) x_1))
(assert (or (or (or (or (or (or x_14 x_13) x_12) x_11) x_10) x_9) x_8))
(assert (or (or (or (or (or (or x_21 x_20) x_19) x_18) x_17) x_16) x_15))
(assert (or (or (or (or (or (or x_28 x_27) x_26) x_25) x_24) x_23) x_22))
(assert (or (or (or (or (or (or x_35 x_34) x_33) x_32) x_31) x_30) x_29))
(assert (or (or (or (or (or (or x_42 x_41) x_40) x_39) x_38) x_37) x_36))
(assert (or (or (or (or (or (or x_49 x_48) x_47) x_46) x_45) x_44) x_43))
(assert (or (or (or (or (or (or x_56 x_55) x_54) x_53) x_52) x_51) x_50))
(check-sat)
